poss:(ES{i}{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}).
EquivRel(possible-event{i:l}
EquivRel(possible-event(poss);_1,_2.R(_1,_2))
 (P:(possible-event{i:l}(poss){i'}), e:possible-event{i:l}(poss).
 (es-knows{i:l}
 (es-knows(poss; R; P; e))
  es-knows{i:l}
  es-knows(poss; R; (e.es-knows{i:l}(poss; R; P; e)); e)) 

latex

Definitions	t  T, P  Q, x:A. B(x), PossibleEvent(poss), f(a), False, A, x:AB(x), , Type, ES, x,y. t(x;y), EquivRel(T;x,y.E(x;y)), Void, K(P)@e, Sym(T;x,y.E(x;y)), x:A  B(x), P & Q, Trans(T;x,y.E(x;y))
Lemmas	not wf, equiv rel wf, event system wf, possible-event wf